package systemfnomabss

object TextualToAbstractTest extends Application {
  val p =   new systemfTextualToAbstractTransform  with AbstractSyntax with TextualSyntax
  import p._
  println  {textualtoabstract(RApp(RLam(RVarName("x"),RTyBool(),RVarName("x")),RIf(RTru(),RFls(),RTru()))) }
  println  {textualtoabstract(RLet(RVarName("x"),RTru(),RLam(RVarName("x"),RTyBool(),RVarName("x")))) }
  println  {textualtoabstract(RLet(RVarName("x"),RTru(),RLam(RVarName("y"),RTyBool(),RVarName("x")))) }
  //(\\f: (int => int) . \\x: bool. \\y: int. (f y)) (\\x: int . x) (true) (5)
  println  {textualtoabstract(RApp(RApp(RApp(
                                RLam(RVarName("f"),RTyArr(RTyInt(),RTyInt()),
                                    RLam(RVarName("x"),RTyBool(),
                                        RLam(RVarName("y"),RTyInt(), RApp(RVarName("f"),RVarName("y"))))),
                                RLam(RVarName("x"),RTyInt(),RVarName("x"))),
                                    RTru()),
                                    	RLit(5)) ) }
  "\\[] X . \\x:X . x"
  println  {textualtoabstract(RTLam(RTyVarName("X"),RLam(RVarName("x"),RTyVarName("X"),RVarName("x")))) }
  
}


trait systemfTextualToAbstractTransform { self : systemfTextualToAbstractTransform with AbstractSyntax with TextualSyntax =>
  //used to convert to form with debruijn indices, adapted for nominal astract syntax by fetching the 'name' instead of the index
  
  //type RawTerm   //merged from ConcreteSyntax
  //type RawType
  
  case class NomNameBinding(n:Name) extends Binding
  
  type CleanTerm = LTerm
  type CleanType = LType
  
  def textualtoabstract(t: RawTerm):CleanTerm= systemfdebruijnify.fresh( t)
  def textualtoabstract(t: RawType):CleanType= systemfdebruijnify.fresh.toDeBruijnType(t)

  object systemfdebruijnify {
    def fresh= new NomAbsifyCtxFun {val ctx = new StringBindingContext[Name](Nil)}
  }
  
  
  trait NomAbsifyCtxFun extends ContextualFun[RawTerm,CleanTerm,NomAbsifyCtxFun]{
    type BindingType =Name
    //type NameCtx = NameBindingContext[NameBinding,Name]
    //val ctxname:NameCtx
    def create(ctxnew: Ctx)=  new NomAbsifyCtxFun {val ctx = ctxnew}

    val hintTransform = {s:String => s}
    def onvar(str:String):BindingType =ctx( ctx.getIndexOfName(str)).getOrElse { throw new Exception("transforming tree to abstract syntax: free variable with name "+str)}
    
  def extendtransformed(str:String,f:String=>String) = throw new Exception()
  
  def extend(str:String,n:Name) = {
    val ctx2 = ctx + (str, n)
    create(ctx2)
  }
  
  @deprecated
  override def extend(str:String):NomAbsifyCtxFun = throw new Exception("using wrong extend function in typechecker")
    
    def apply(t:RawTerm):CleanTerm = toDeBruijn(t) 

    def toDeBruijn(t: RawTerm):CleanTerm =  t match {  
        //case ty: RType            => toDeBruijnType(ty)
        case RTru()               => Tru()
        case RFls()               => Fls()
        case RLit(n)              => Lit(n)
        case RUnit()              => Unit()
        
        case RIf(cond,pos,neg)   => If(this(cond),this(pos),this(neg))
        case RLam(RVarName(str), ty,t) =>  val n=Name(str);Lam(toDeBruijnType(ty), n \\ extend(str,n)(t))
        case RVarName(str) =>  Var(onvar(str))
        case RLet(RVarName(str),conc:RawTerm,body:RawTerm) =>
           val n=Name(str); Let(toDeBruijn(conc), n \\ extend(str,n).toDeBruijn(body))
        case RApp(t1,t2)                => App(this (t1), this (t2))
        
        case RTLam(RTyVarName(str), t) => val n=Name(str);TLam(n \\ extend(str,n)(t))
        case RTApp(t1,ty2)          => TApp(this(t1),toDeBruijnType(ty2))
        
        
        case RPack(implty:RawType,implterm:RawTerm, pubty:RawType) => {
          Pack(toDeBruijnType(implty),this(implterm),toDeBruijnType(pubty))
          }
        case RUnpack(impl:RawTerm,wrappubty:RawTerm,wrappubterm:RawTerm,body:RawTerm) => (wrappubty,wrappubterm) match { 
          case (RTyVarName(pubtystr),RVarName(pubtermstr)) => {
          val pubTy = Name(pubtystr); val pubTerm = Name(pubtermstr)
          val cleanbody = extend(pubtystr,pubTy).extend(pubtermstr,pubTerm)(body)
          Unpack(this(impl),pubTy\\(
                                   Lam(TyVar(pubTy), pubTerm\\ (
                                                      cleanbody))))
          }}
        
        case RRecProj(t1:RawTerm,label)                 => RecProj(this (t1),label)
        case r@RRecord(fields:List[(String,RawTerm)])   => Record(fields.map( {case (str,rt) => (str,this(rt))}))
        case _ => throw new Exception("cannot parse raw tree "+t)
        
     }
    val toDeBruijnType:RawType=>CleanType = new (RawType=>CleanType){
      def apply(r:RawType) = r match {
        case RTyBool() => TyBool()
        case RTyInt()  => TyInt()
        case RTyUnit() => TyUnit()
        case r@RTyRecord(fields:List[(String, RawType)]) => TyRecord(fields.map( {case (s,r)=> val cleanty = this(r); (s,cleanty)}))
        
        case RTyArr(ty1:RawType,ty2:RawType)           => TyArr(this(ty1),this(ty2)) 
        case RTyUniv(RTyVarName(hint),ty:RawType) => val n=Name(hint);TyUniv( n \\extend(hint,n).toDeBruijnType(ty))
        case RTyExist(RTyVarName(x), ty:RawType)     => {
          val n=Name(x);
          TyExist(n \\ extend(x,n).toDeBruijnType(ty))
        }
        case RTyVarName(str) => TyVar(onvar(str))
        case _ => throw new Exception("cannot parse raw tree "+r)
        }

    }
    
    

  
  }


}








